The Free On-line Dictionary of Computing (30 December 2018):

SPARK Annotation Language

    (SAL) ICL, Ltd.  Used in the verification of
   SPARK programs against Z specifications.

   (1994-12-08)